/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXB30





␈↓ α∧␈↓↓␈↓ β Automatic Program Generation from Logic Specifications



␈↓ α∧␈↓It␈α
has␈α
been␈α
observed␈α
that␈α
an␈α
algorithm␈α
consists␈α
of␈α
two␈α
separable␈α
components:␈αlogic

␈↓ α∧␈↓and␈α∪control.␈α∀ The␈α∪description␈α∀of␈α∪an␈α∀algorithm,␈α∪specifying␈α∀its␈α∪logic␈α∀and␈α∪control

␈↓ α∧␈↓components,␈α⊂can␈α⊂be␈α⊂programming-language-independent.␈α⊂ We␈α⊂have␈α⊃designed␈α⊂and

␈↓ α∧␈↓implemented␈α⊂a␈α∂system␈α⊂that␈α⊂accepts␈α∂logic␈α⊂specifications,␈α∂generates␈α⊂algorithms␈α⊂in␈α∂an

␈↓ α∧␈↓intermediate␈αlanguage,␈α
and␈αthen␈αtranslates␈α
these␈αalgorithms␈α
into␈αprograms␈αin␈α
specific

␈↓ α∧␈↓target languages.

␈↓ α∧␈↓This␈αsystem␈α
is␈αunique␈α
in␈αits␈αability␈α
to␈αgenerate␈α
programs␈αin␈α
more␈αthan␈αone␈α
language.

␈↓ α∧␈↓Moreover,␈α∞it␈α
represents␈α∞a␈α
large␈α∞non-trivial␈α
application␈α∞of␈α
formal␈α∞techniques.␈α
Many

␈↓ α∧␈↓programs␈α⊂of␈α⊂varying␈α⊂sizes␈α⊂have␈α⊃been␈α⊂specified␈α⊂and␈α⊂generated␈α⊂by␈α⊂the␈α⊃system,␈α⊂the

␈↓ α∧␈↓largest being the system itself.

␈↓ α∧␈↓In␈α⊃section␈α⊃I␈α⊃we␈α⊂explain␈α⊃the␈α⊃rationale␈α⊃for␈α⊂approaching␈α⊃the␈α⊃problem␈α⊃of␈α⊂obtaining

␈↓ α∧␈↓correct␈α
programs␈α
as␈α
we␈α
have,␈α
from␈α
logic␈α
specifications␈α
to␈α
equivalent␈αprogram.␈α
Section

␈↓ α∧␈↓II␈αdescribes␈α
the␈αspecification␈α
language␈αinformally,␈α
a␈αformal␈α
treatment␈αbeing␈α
available

␈↓ α∧␈↓elsewhere.␈α⊂In␈α∂sections␈α⊂III␈α∂and␈α⊂IV␈α⊂we␈α∂show␈α⊂how␈α∂a␈α⊂specification␈α∂is␈α⊂mapped␈α⊂into␈α∂a

␈↓ α∧␈↓deterministic␈αalgorithm,␈αand␈α
outline␈αthe␈αproof␈α
that␈αthe␈αalgorithm␈α
generated␈αsatisfies

␈↓ α∧␈↓the␈αspecification.␈αSection␈αV␈αcontains␈αconclusions␈αthat␈αcan␈αbe␈αdrawn␈αfrom␈αthis␈αeffort,

␈↓ α∧␈↓as well as directions for continuing research.




␈↓ α∧␈↓␈↓ ¬NRuth E. Davis
␈↓ α∧␈↓␈↓ ¬3EECS Department
␈↓ α∧␈↓␈↓ ¬∧University of Santa Clara
␈↓ α∧␈↓␈↓ ¬∃Santa Clara, CA 95053